Nuprl Lemma : isint-int
11,40
postcript
pdf
z
:
,
a
,
b
:top. sqequal(isint(
z
;
a
;
b
);
a
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
z:
, a,b:top. sqequal(isint(z;a;b); a) z:, a,b:top. sqequal(isint(z;a;b); a) 
Tx:A. B(x)